VERS5 
NIL 
((SIMPINFO BIRD#2)) (|∀AB FLIES.A(AB,FLIES)≡ (∀X.¬AB(ASPECT1(X))⊃¬FLIES(X))∧(∀X.BIRD(X)⊃AB(ASPECT1(X)))∧ (∀X.BIRD(X)∧¬AB(ASPECT2(X))⊃FLIES(X))∧ (∀X.OSTRICH(X)⊃AB(ASPECT2(X)))∧ (∀X.OSTRICH(X)∧¬AB(ASPECT3(X))⊃¬FLIES(X))| . (DEFINE A (TM& . |∀AB FLIES.A(AB,FLIES)≡ (∀X.¬AB(ASPECT1(X))⊃¬FLIES(X))∧(∀X.BIRD(X)⊃AB(ASPECT1(X)))∧ (∀X.BIRD(X)∧¬AB(ASPECT2(X))⊃FLIES(X))∧ (∀X.OSTRICH(X)⊃AB(ASPECT2(X)))∧ (∀X.OSTRICH(X)∧¬AB(ASPECT3(X))⊃¬FLIES(X))|) NIL) . ((ASPECT3 . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . BIRD#1 . NIL . VARIABLE .)) (OSTRICH . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . BIRD#1 . NIL . VARIABLE .)) (ASPECT2 . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . BIRD#1 . NIL . VARIABLE .)) (BIRD . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . BIRD#1 . NIL . VARIABLE .)) (ASPECT1 . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . BIRD#1 . NIL . VARIABLE .)) (X . (GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . BIRD#1 . NIL . VARIABLE .)) (A . (|((GROUND→TRUTHVAL)⊗(GROUND→TRUTHVAL))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . BIRD#1 . NIL . DEFINED .)) (FLIES . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . BIRD#1 . NIL . VARIABLE .)) (AB . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . BIRD#1 . NIL . VARIABLE .))) . NIL . (BIRD#1) . NIL . BIRD . NIL . 1 .)(|(∀X Y.¬ASPECT1(X)=ASPECT2(Y))∧(∀X Y.¬ASPECT1(X)=ASPECT3(Y))∧(∀X Y.¬ASPECT2(X)=ASPECT3(Y))∧(∀X Y.ASPECT1(X)=ASPECT1(Y)≡X=Y)∧(∀X Y.ASPECT2(X)=ASPECT2(Y)≡X=Y)∧(∀X Y.ASPECT3(X)=ASPECT3(Y)≡X=Y)| . (AXIOM (TM& . |(∀X Y.¬ASPECT1(X)=ASPECT2(Y))∧(∀X Y.¬ASPECT1(X)=ASPECT3(Y))∧(∀X Y.¬ASPECT2(X)=ASPECT3(Y))∧(∀X Y.ASPECT1(X)=ASPECT1(Y)≡X=Y)∧(∀X Y.ASPECT2(X)=ASPECT2(Y)≡X=Y)∧(∀X Y.ASPECT3(X)=ASPECT3(Y)≡X=Y)|)) . (ASPECT3 OSTRICH ASPECT2 BIRD ASPECT1 X A FLIES AB (Y . (GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . BIRD#2 . NIL . VARIABLE .))) . NIL . (BIRD#2) . NIL . BIRD . NIL . 2 .)(|∀AB FLIES.A1(AB,FLIES)≡ A(AB,FLIES)∧ (∀AB1 FLIES1.A(AB1,FLIES1)∧(∀Z.AB1(Z)⊃AB(Z))⊃(∀Z.AB(Z)≡AB1(Z)))| . (DEFINE A1 (TM& . |∀AB FLIES.A1(AB,FLIES)≡ A(AB,FLIES)∧ (∀AB1 FLIES1.A(AB1,FLIES1)∧(∀Z.AB1(Z)⊃AB(Z))⊃(∀Z.AB(Z)≡AB1(Z)))|) NIL) . (ASPECT3 OSTRICH ASPECT2 BIRD ASPECT1 X A FLIES AB (Z . (GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . BIRD#3 . NIL . VARIABLE .)) (FLIES1 . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 1000)) . BIRD#3 . NIL . VARIABLE .)) (AB1 . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 1000)) . BIRD#3 . NIL . VARIABLE .)) (A1 . (|((GROUND→TRUTHVAL)⊗(GROUND→TRUTHVAL))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 1000)) . BIRD#3 . NIL . DEFINED .))) . NIL . (BIRD#3 BIRD#2) . NIL . BIRD . NIL . 3 .)(|A1(AB,FLIES)| . (ASSUME (TM& . |A1(AB,FLIES)|)) . (ASPECT3 OSTRICH ASPECT2 BIRD ASPECT1 X A FLIES AB Z FLIES1 AB1 A1) . NIL . (BIRD#4) . NIL . BIRD . NIL . 4 .)(|∀X.FLIES2(X)≡BIRD(X)∧¬OSTRICH(X)| . (DEFINE FLIES2 (TM& . |∀X.FLIES2(X)≡BIRD(X)∧¬OSTRICH(X)|) NIL) . (ASPECT3 OSTRICH ASPECT2 BIRD ASPECT1 X A FLIES AB (FLIES2 . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 1000)) . BIRD#5 . NIL . DEFINED .))) . NIL . (BIRD#5 BIRD#2) . NIL . BIRD . NIL . 5 .)(|∀Z.AB2(Z)≡(∃X.BIRD(X)∧Z=ASPECT1(X))∨(∃X.OSTRICH(X)∧Z=ASPECT2(X))| . (DEFINE AB2 (TM& . |∀Z.AB2(Z)≡(∃X.BIRD(X)∧Z=ASPECT1(X))∨(∃X.OSTRICH(X)∧Z=ASPECT2(X))|) NIL) . (ASPECT3 OSTRICH ASPECT2 BIRD ASPECT1 X A FLIES AB Z FLIES1 AB1 A1 (AB2 . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 1000)) . BIRD#6 . NIL . DEFINED .))) . NIL . (BIRD#6 BIRD#2) . NIL . BIRD . NIL . 6 .)(|A(AB,FLIES)∧(∀AB1 FLIES1.A(AB1,FLIES1)∧(∀Z.AB1(Z)⊃AB(Z))⊃(∀Z.AB(Z)≡AB1(Z)))| . (RW (LN& . BIRD#4) (OPEN A1)) . (A FLIES AB Z FLIES1 AB1) . NIL . (BIRD#4 BIRD#2) . NIL . BIRD . NIL . 7 .)(|A(AB,FLIES)| . (TRW (TM& . |A(AB,FLIES)|) (USE (LR& BIRD#7))) . (ASPECT3 OSTRICH ASPECT2 BIRD ASPECT1 X A FLIES AB) . NIL . (BIRD#4 BIRD#2) . NIL . BIRD . NIL . 8 .)(|∀AB1 FLIES1.A(AB1,FLIES1)∧(∀Z.AB1(Z)⊃AB(Z))⊃(∀Z.AB(Z)≡AB1(Z))| . (TRW (TM& . |∀AB1 FLIES1.A(AB1,FLIES1)∧(∀Z.AB1(Z)⊃AB(Z))⊃(∀Z.AB(Z)≡AB1(Z))|) (USE (LR& BIRD#7))) . (ASPECT3 OSTRICH ASPECT2 BIRD ASPECT1 X A FLIES AB Z FLIES1 AB1 A1) . NIL . (BIRD#4 BIRD#2) . NIL . BIRD . NIL . 9 .)(|(∀X.¬AB(ASPECT1(X))⊃¬FLIES(X))∧(∀X.BIRD(X)⊃AB(ASPECT1(X)))∧(∀X.BIRD(X)∧¬AB(ASPECT2(X))⊃FLIES(X))∧(∀X.OSTRICH(X)⊃AB(ASPECT2(X)))∧(∀X.OSTRICH(X)∧¬AB(ASPECT3(X))⊃¬FLIES(X))| . (RW (LN& . BIRD#8) (OPEN A)) . (ASPECT3 OSTRICH ASPECT2 BIRD ASPECT1 X FLIES AB) . NIL . (BIRD#4 BIRD#2) . NIL . BIRD . NIL . 10 .)(|AB2(Z)| . (ASSUME (TM& . |AB2(Z)|)) . (ASPECT3 OSTRICH ASPECT2 BIRD ASPECT1 X A FLIES AB Z FLIES1 AB1 A1 AB2) . NIL . (BIRD#11) . NIL . BIRD . NIL . 11 .)(|(∃X.BIRD(X)∧Z=ASPECT1(X))∨(∃X.OSTRICH(X)∧Z=ASPECT2(X))| . (RW (LN& . BIRD#11) (OPEN AB2)) . (OSTRICH ASPECT2 BIRD ASPECT1 X Z) . NIL . (BIRD#11 BIRD#2) . NIL . BIRD . NIL . 12 .)(|AB(Z)| . (DERIVE (TM& . |AB(Z)|) ((LR& BIRD#12 BIRD#10)) NIL) . (ASPECT3 OSTRICH ASPECT2 BIRD ASPECT1 X A FLIES AB Z FLIES1 AB1 A1) . NIL . (BIRD#4 BIRD#11 BIRD#2) . NIL . BIRD . NIL . 13 .)(|AB2(Z)⊃AB(Z)| . (CI ((LR& BIRD#11)) (LN& . BIRD#13) NIL) . (AB Z AB2) . NIL . (BIRD#4 BIRD#2) . NIL . BIRD . NIL . 14 .)(|∀Z.AB2(Z)⊃AB(Z)| . (DERIVE (TM& . |∀Z.AB2(Z)⊃AB(Z)|) ((LR& BIRD#14)) NIL) . (ASPECT3 OSTRICH ASPECT2 BIRD ASPECT1 X A FLIES AB Z FLIES1 AB1 A1 AB2) . NIL . (BIRD#4 BIRD#2) . NIL . BIRD . NIL . 15 .)(|(∀X.¬AB2(ASPECT1(X))⊃¬FLIES2(X))∧(∀X.BIRD(X)⊃AB2(ASPECT1(X)))∧(∀X.BIRD(X)∧¬AB2(ASPECT2(X))⊃FLIES2(X))∧(∀X.OSTRICH(X)⊃AB2(ASPECT2(X)))∧(∀X.OSTRICH(X)∧¬AB2(ASPECT3(X))⊃¬FLIES2(X))| . (DERIVE (TM& . |(∀X.¬AB2(ASPECT1(X))⊃¬FLIES2(X))∧(∀X.BIRD(X)⊃AB2(ASPECT1(X)))∧(∀X.BIRD(X)∧¬AB2(ASPECT2(X))⊃FLIES2(X))∧(∀X.OSTRICH(X)⊃AB2(ASPECT2(X)))∧(∀X.OSTRICH(X)∧¬AB2(ASPECT3(X))⊃¬FLIES2(X))|) ((LR&)) (OPEN AB2 FLIES2)) . (ASPECT3 OSTRICH ASPECT2 BIRD ASPECT1 X A FLIES AB Z FLIES1 AB1 A1 FLIES2 AB2) . NIL . (BIRD#6 BIRD#5 BIRD#2) . NIL . BIRD . NIL . 16 .)(|A(AB2,FLIES2)≡(∀X.¬AB2(ASPECT1(X))⊃¬FLIES2(X))∧(∀X.BIRD(X)⊃AB2(ASPECT1(X)))∧(∀X.BIRD(X)∧¬AB2(ASPECT2(X))⊃FLIES2(X))∧(∀X.OSTRICH(X)⊃AB2(ASPECT2(X)))∧(∀X.OSTRICH(X)∧¬AB2(ASPECT3(X))⊃¬FLIES2(X))| . (UE (UELST& (AB . AB2) (FLIES . FLIES2)) (LN& . BIRD#1) NIL) . (ASPECT3 OSTRICH ASPECT2 BIRD ASPECT1 X A FLIES AB Z FLIES1 AB1 A1 FLIES2 AB2) . NIL . (BIRD#1 BIRD#2) . NIL . BIRD . NIL . 17 .)(|A(AB2,FLIES2)| . (RW (LN& . BIRD#17) (USE (LR& BIRD#16))) . (A FLIES2 AB2) . NIL . (BIRD#6 BIRD#5 BIRD#1 BIRD#2) . NIL . BIRD . NIL . 18 .)(|∀Z.AB(Z)≡AB2(Z)| . (DERIVE (TM& . |∀Z.AB(Z)≡AB2(Z)|) ((LR& BIRD#9 BIRD#15 BIRD#18)) NIL) . (ASPECT3 OSTRICH ASPECT2 BIRD ASPECT1 X A FLIES AB Z FLIES1 AB1 A1 AB2) . NIL . (BIRD#6 BIRD#1 BIRD#4 BIRD#2) . NIL . BIRD . NIL . 19 .)(|(∀X.¬(∃X1.BIRD(X1)∧X=X1)⊃¬FLIES(X))∧(∀X.BIRD(X)∧¬(∃X2.OSTRICH(X2)∧X=X2)⊃FLIES(X))∧(∀X.OSTRICH(X)⊃¬FLIES(X))| . (RW (LN& . BIRD#8) ((USE (LR& BIRD#1) MODE: EXACT) ((USE (LR& BIRD#19) MODE: EXACT) (OPEN AB2)))) . (OSTRICH BIRD X FLIES (X1 . (GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . BIRD#20 . NIL . VARIABLE .)) (X2 . (GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . BIRD#20 . NIL . VARIABLE .))) . NIL . (BIRD#4 BIRD#2) . NIL . BIRD . NIL . 20 .)(|∀X.FLIES(X)≡BIRD(X)∧¬OSTRICH(X)| . (DERIVE (TM& . |∀X.FLIES(X)≡BIRD(X)∧¬OSTRICH(X)|) ((LR& BIRD#20)) NIL) . (ASPECT3 OSTRICH ASPECT2 BIRD ASPECT1 X A FLIES AB) . NIL . (BIRD#4 BIRD#2) . NIL . BIRD . NIL . 21 .)